|
|
String Analysis for Code Contracts
Dort, Vlastimil ; Parízek, Pavel (vedoucí práce) ; Kofroň, Jan (oponent)
Jedním ze způsobů prevence chyb v objektově orientovaných programech je používání kontraktů, kterými jsou například vstupní a výstupní podmínky metod nebo invarianty tříd. Ve frameworku .NET je používání kontraktů umožněno díky frameworku Code Contracts, který mimo jiné obsahuje nástroj Clousot na statickou analýzu programů, založený na abstraktní interpretaci. Ačkoli řetězce jsou jedním ze základních typů v programech pro .NET, Clousot neobsahuje použitelnou podporu pro analýzu řetězcových hodnot. V této práci probereme specifika práce s řetězci v jazyce C# a frameworku .NET a ukážeme, jak je možné ji pokrýt statickou analýzou. Zvolený přístup využívá metody třídy String a omezenou podmnožinu regulárních výrazů ke specifikaci vlastností řetězců v kódu, a abstraktní interpretaci s nerelačními abstraktními doménami k důkazům těchto vlastností. Zvolili jsme několik již publikovaných abstraktních domén pro řetězce, které se mezi sebou liší složitostí a schopností reprezentovat různé vlastnosti řetězců. Tyto domény jsme adaptovali pro zvolené prostředí, což zahrnovalo definici abstraktní sémantiky pro podporované řetězcové operace. Abstraktní domény jsme implementovali v nástroji Clousot, a to tak, aby bylo v budoucnu možné rozšíření o další domény. Powered by TCPDF (www.tcpdf.org)
|
|
|
Ověřování integritních omezení v C# pomocí Code Contracts
Dort, Vlastimil ; Malý, Jakub (vedoucí práce) ; Ježek, Pavel (oponent)
Jazyk OCL slouží pro specifikaci integritních omezení nad modelem jazyka UML, Code Contracts umožňují integritní omezení zapsat v programovacích jazycích pro platforum Microsoft .NET Framework. Cílem předložené práce je najít a implementovat překlad integritních omezení z jazyka OCL do programovacího jazyka C# s využitím Code Contracts. Představeny jsou možnosti technologie Code Contracts a jazyka OCL, jednotlivé jazykové konstrukce a operace ze standardní knihovny jazyka OCL jsou pak porovnány se syntakticky a sémanticky obdobnými vyjádřeními v jazyce C#. Zvolený překlad se snaží tam, kde je to možné, dodržovat sémantiku jazyka OCL. Generování zdrojových kódů v jazyce C# s Code Contracts je implementováno do programu eXolutio, ze kterého je využit editor diagramů tříd a parser jazyka OCL. Powered by TCPDF (www.tcpdf.org)
|
host ::
RSS.